The present application describes systems and methods relating to information flow tracking and detection of unintentional design flaws of digital devices and microprocessor systems. In some instances the disclosed techniques and systems involve hardware security, trust and protection from unintentional design flaws, such as hardware Trojans.
In the computing environment, the presence of malicious attacks and exploited system vulnerabilities can become problematic, causing damaging effects to computer hardware components. Therefore, hardware security is becoming of increasing importance in the microprocessor and semiconductor industries. Current hardware security techniques typically utilize manual processes for implementing certain security aspects of the hardware design, for example information flow control.
Hardware design and supply can involve multiple teams spread around the world. In this distributed process, hardware may be intentionally or unintentionally built with unspecified functionality. Such undocumented modifications can provide a hidden channel to leak sensitive information or a back door for attackers to compromise a system.
In some instances, malicious attacks can include threats directly implemented via hardware components, such as Hardware Trojans. Hardware Trojans are a major security threat originating from malicious design modifications. These are carefully designed lightweight components that are activated under rare conditions, which protects them from being detected during the design phase. As a consequence, these hard-to-detect hidden time bombs are often identified only after severe damage has been inflicted.
Prior efforts to detect hardware Trojans include exhaustive testing, which becomes intractable even for moderate scale designs. More intelligent methods utilize integrated circuit test methodologies to increase the transition probability of the Troj an trigger or to identify redundant circuit with low switching probabilities. However, testing is a hard problem even when not considering intentionally difficult to activate logic. A number of methods seek to capture the Trojan behaviors using side channel signal analysis (e.g., they attempt to detect transient power and spurious delays added to the design due to the Trojan design). The increasing amount of hardware manufacturing process variation and decreases in the size of the Trojan payload can mitigate the effectiveness of these techniques.
Detecting Trojans in IP cores is an extremely challenging task. Many existing methods for detecting Trojans in IP cores rely on testing or verification methods to identify suspicious signals, e.g., those with extremely low transition probability. However, these methods may still miss certain types of Trojans, e.g., a Trojan without a trigger signal. Some methods detect Trojans by formally proving security related properties. They indicate the existence of a Trojan when a security property is violated. However, these methods typically require rewriting the hardware design in a formal language, which comes at significant design cost. Additionally, most of the existing methods may not provide clues (e.g., revealing Trojan behavior) that will help pinpoint the Trojan from the entire design.
Hardware trust is an emerging security threat due to the globalization of hardware supply chain. A major security concern is Trojan horses inserted by an untrusted party. Hardware Trojans are carefully crafted to protect them from being identified, and detecting them in third party intellectual property (IP) cores requires significant effort. This work employs information flow tracking to discover hardware Trojans. It works by identifying Trojans that violate the confidentiality and integrity properties of these hardware components. Our method is able to formally prove the existence of such types of Trojans without activating them. We demonstrate our techniques on trust-HUB benchmarks and show that our method precisely detects the hardware Trojans that violate the information flow security properties related to confidentiality and integrity.
Existing hardware Trojan detection methods generally fall into two categories: invasive and non-invasive. Invasive methods either insert test points in the design for increased observability or use reverse engineering techniques to check for malicious design modification at the physical level. These methods are relatively expensive since they require highly specialized tool for physical access to the chip layout. Non-invasive methods do not need to modify the design. They look for clues, e.g., faulty output, downgraded performance, and increased power consumption, which may reveal the existence of a Trojan. Some existing methods try to capture these clues by functional testing, while others perform circuit parameter characterization.
It may be desirable to implement a formal method for detecting unintentional design flaws, such as hardware Trojans, by proving security properties related to confidentiality and integrity.